perm filename SEXP[BMP,SYS] blob
sn#642941 filedate 1982-02-24 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00007 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 I have just succeeded in making the theorem prover go into and infintie
C00004 00003 DEFN(SL (U V)
C00005 00004 DEFN(SUBEXP (X Y)
C00011 00005 DEFN(HOMEO (X Y)
C00019 00006 Informal proof of TRANSITIVITY OF HOMEO
C00022 00007 DEFN(TRANS.HOMEO (X Y Z) (IF (HOMEO X Y) (IF (HOMEO Y Z) (HOMEO X Z) T) T))
C00047 ENDMK
C⊗;
I have just succeeded in making the theorem prover go into and infintie
rewrite loop. Saves me from have to prove it total!
See below
DEFN(LEFT (X) (IF (LISTP X) (LEFT (CAR X)) X)))
The lemma CAR.LESSP establishes that (COUNT X) goes down according
to the well-founded function LESSP in each recursive call. Hence, LEFT
is accepted under the principle of definition.
[922 cns / 2.1 s + 0.0 gc + .2 io (= 13 @ 2)]
LEFT
16:
PROVE.LEMMA(LEFT.HACK (REWRITE) (EQUAL (LEFT X) (IF(LISTP X)(LEFT (CAR X))X)))
This conjecture simplifies, expanding the definition of LEFT, to:
T.
Q.E.D.
[647 cns / .9 s + 0.0 gc + .1 io (= 3 @ 1)]
LEFT.HACK
17:
PROVE((EQUAL (LEFT X) X))
***ERROR***
STACK OVERFLOW
NIL
(REWRITE.FNCALL broken)
18:
DEFN(SL (U V)
(IF (AND (LISTP U)(LISTP V))
(SL (CDR U) (CDR V))
(AND (NOT (LISTP U)) (NOT (LISTP V))) ))
DEFN(APPEND (U V) (IF (LISTP U) (CONS (CAR U) (APPEND (CDR U) V)) V))
DEFN(REVERSE (U) (IF (LISTP U) (APPEND (REVERSE (CDR U)) (CONS (CAR U) 0)) 0))
PROVE((SL U (REVERSE U)))
DEFN(SUBEXP (X Y)
(IF (LISTP Y)
(OR (EQUAL X Y) (SUBEXP X (CAR Y)) (SUBEXP X (CDR Y)))
(EQUAL X Y)) )
The lemmas CAR.LESSP and CDR.LESSP establish that (COUNT Y)
decreases according to the well-founded function LESSP in each
recursive call. Hence, SUBEXP is accepted under the principle of
definition. Note that (OR (FALSEP (SUBEXP X Y)) (TRUEP (SUBEXP X Y)))
is a theorem.
[2692 cns / 2.2 s + 0.0 gc + .2 io (= 6 @ 0)]
(SUBEXP)
12←
PROVE( (IMPLIES (AND (NOT (SUBEXP X Z)) (SUBEXP Y Z)) (NOT (SUBEXP X Y))) )
This conjecture can be simplified, using the abbreviations NOT, AND,
and IMPLIES, to the conjecture:
(IMPLIES (AND (NOT (SUBEXP X Z)) (SUBEXP Y Z))
(NOT (SUBEXP X Y))),
which we will name *1.
We will try to prove it by induction. Three inductions are
suggested by terms in the conjecture. They merge into two likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP Z)) (p X Y Z))
(IMPLIES (AND (LISTP Z)
(p X Y (CDR Z))
(p X Y (CAR Z)))
(p X Y Z))).
The inequalities CAR.LESSP and CDR.LESSP establish that the measure
(COUNT Z) decreases according to the well-founded function LESSP in the
induction step of the scheme. The above induction scheme generates the
following five new goals:
Case 5. (IMPLIES (AND (NOT (LISTP Z))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))).
This simplifies, opening up the function SUBEXP, to:
(IMPLIES (AND (NOT (LISTP Z))
(NOT (EQUAL X Z))
(EQUAL Y Z))
(NOT (EQUAL X Y))).
Of course, this simplifies again, clearly, to:
T.
collecting lists
9770, 10282 free cells
Case 4. (IMPLIES (AND (LISTP Z)
(SUBEXP X (CDR Z))
(SUBEXP X (CAR Z))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))).
This simplifies, opening up the function SUBEXP, to:
T.
Case 3. (IMPLIES (AND (LISTP Z)
(NOT (SUBEXP Y (CDR Z)))
(SUBEXP X (CAR Z))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))).
This simplifies, expanding the definition of SUBEXP, to:
T.
Case 2. (IMPLIES (AND (LISTP Z)
(SUBEXP X (CDR Z))
(NOT (SUBEXP Y (CAR Z)))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))),
which simplifies, opening up SUBEXP, to:
T.
Case 1. (IMPLIES (AND (LISTP Z)
(NOT (SUBEXP Y (CDR Z)))
(NOT (SUBEXP Y (CAR Z)))
(NOT (SUBEXP X Z))
(SUBEXP Y Z))
(NOT (SUBEXP X Y))).
This simplifies, unfolding the function SUBEXP, to:
(IMPLIES (AND (LISTP Z)
(NOT (SUBEXP Y (CDR Z)))
(NOT (SUBEXP Y (CAR Z)))
(NOT (EQUAL X Z))
(NOT (SUBEXP X (CAR Z)))
(NOT (SUBEXP X (CDR Z)))
(EQUAL Y Z))
(NOT (SUBEXP X Y))),
which again simplifies, expanding the definition of SUBEXP, to:
T.
That finishes the proof of *1. Q.E.D.
PROVED
13←
DEFN(HOMEO (X Y)
(IF (LISTP Y)
(OR (HOMEO X (CAR Y))
(HOMEO X (CDR Y))
(AND (LISTP X) (HOMEO (CAR X) (CAR Y)) (HOMEO (CDR X) (CDR Y))) )
(EQUAL X Y) ))
collecting lists
9135, 10159 free cells
The lemmas CAR.LESSP and CDR.LESSP can be used to prove that
(COUNT Y) goes down according to the well-founded function LESSP in
each recursive call. Hence, HOMEO is accepted under the principle of
definition. Observe that (OR (FALSEP (HOMEO X Y)) (TRUEP (HOMEO X Y)))
is a theorem.
[5437 cns / 6.1 s + 2.6 gc + .2 io (= 13 @ 1)]
HOMEO
4←
PROVE( (IMPLIES (EQUAL X Y) (HOMEO X Y)) )
This conjecture can be simplified, using the abbreviation IMPLIES, to
the conjecture:
(IMPLIES (EQUAL X Y) (HOMEO X Y)),
which we simplify, clearly, to:
(HOMEO Y Y).
Give the above formula the name *1.
Let us appeal to the induction principle. There is only one
plausible induction. We will induct according to the following scheme:
(AND (IMPLIES (NOT (LISTP Y)) (p Y))
(IMPLIES (AND (LISTP Y)
(p (CDR Y))
(p (CAR Y)))
(p Y))).
The inequalities CAR.LESSP and CDR.LESSP establish that the measure
(COUNT Y) decreases according to the well-founded function LESSP in the
induction step of the scheme. The above induction scheme produces two
new formulas:
Case 2. (IMPLIES (NOT (LISTP Y)) (HOMEO Y Y)).
This simplifies, opening up the definition of HOMEO, to:
T.
Case 1. (IMPLIES (AND (LISTP Y)
(HOMEO (CDR Y) (CDR Y))
(HOMEO (CAR Y) (CAR Y)))
(HOMEO Y Y)).
This simplifies, opening up the function HOMEO, to:
T.
That finishes the proof of *1. Q.E.D.
PROVED
5←
PROVE( (IMPLIES (AND (HOMEO X Y) (HOMEO Y Z)) (HOMEO X Z)) )
This formula can be simplified, using the abbreviations AND and IMPLIES,
to:
(IMPLIES (AND (HOMEO X Y) (HOMEO Y Z))
(HOMEO X Z)),
which we will name *1.
We will try to prove it by induction. Three inductions are
suggested by terms in the conjecture. They merge into two likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP Z)) (p X Z Y))
(IMPLIES (AND (LISTP Z)
(p (CDR X) (CDR Z) (CDR Y))
(p (CAR X) (CAR Z) (CAR Y))
(p X (CDR Z) Y)
(p X (CAR Z) Y))
(p X Z Y))).
The inequalities CAR.LESSP and CDR.LESSP establish that the measure
(COUNT Z) decreases according to the well-founded function LESSP in the
induction step of the scheme. Note, however, the inductive instances
chosen for X and Y. The above induction scheme produces the following
37 new conjectures:
DEFN(HO (X Y Z)
(IF (LISTP Z)
(OR (HO X Y (CAR Z))
(HO X Y (CDR Z))
(AND (LISTP Y)
(OR (HO X (CAR Y) (CAR Z))
(HO X (CDR Y) (CDR Z))
(AND (LISTP X)
(HO (CAR X) (CAR Y) (CAR Z))
(HO (CDR X) (CDR Y) (CDR Z)) ) )) )
T ))
The lemmas CAR.LESSP and CDR.LESSP can be used to prove that
(COUNT Z) goes down according to the well-founded function LESSP in
each recursive call. Hence, HO is accepted under the principle of
definition. Observe that (TRUEP (HO X Y Z)) is a theorem.
[9188 cns / 8.4 s + 0.0 gc + .3 io (= 35 @ 2)]
(HO)
9←
PROVE( (EQUAL (IMPLIES (AND (HOMEO X Y) (HOMEO Y Z)) (HOMEO X Z))
(HO X Y Z) ) )
collecting lists
9623, 10135 free cells
This conjecture simplifies, expanding the definitions of AND, IMPLIES,
and HO, to:
(IMPLIES (AND (HOMEO X Y) (HOMEO Y Z))
(HOMEO X Z)).
Name the above subgoal *1.
We will try to prove it by induction. Three inductions are
suggested by terms in the conjecture. They merge into two likely
candidate inductions. However, only one is unflawed. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP Z)) (p X Z Y))
(IMPLIES (AND (LISTP Z)
(p (CDR X) (CDR Z) (CDR Y))
(p (CAR X) (CAR Z) (CAR Y))
(p X (CDR Z) Y)
(p X (CAR Z) Y))
(p X Z Y))).
The inequalities CAR.LESSP and CDR.LESSP establish that the measure
(COUNT Z) decreases according to the well-founded function LESSP in the
induction step of the scheme. Note, however, the inductive instances
chosen for X and Y. The above induction scheme produces the following
37 new conjectures:
***CTRL-F ABORT***
************** F A I L E D **************
NIL
11←
???
DEFN(TRANS.HOMEO (X Y Z) (IF (HOMEO X Y) (IF (HOMEO Y Z) (HOMEO X Z) T) T))
PROVE( (EQUAL (TRANS.HOMEO X Y Z) (HO X Y Z)) )
Informal proof of TRANSITIVITY OF HOMEO
HOMEO (X Y) <=
(IF (LISTP Y)
(OR (HOMEO X (CAR Y))
(HOMEO X (CDR Y))
(AND (LISTP X) (HOMEO (CAR X) (CAR Y)) (HOMEO (CDR X) (CDR Y))) )
(EQUAL X Y) ))
Show HOMEO[X Y]∧ HOMEO[Y Z]->HOMEO[X Z]
By induction on Z (CDR[Z] << Z)
Case0 ¬LISTP[Z] ∧ HOMEO[X Y]∧ HOMEO[Y Z]
=> Y=Z
=> ¬LISTP[Y)
=> X=Y
=> X=Z
Case1 LISTP[Z] ∧ HOMEO[X Y]∧ HOMEO[Y Z]
Casee1.1 HOMEO[Y,CAR Z]
=> HOMEO[X Y]∧ HOMEO[Y CAR Z]->HOMEO[X CAR Z] (INDHYP)
=> HOMEO[X,CAR Z]
=> HOMEO[X,Z]
Casee1.2 HOMEO[Y,CDR Z]
=> HOMEO[X Y]∧ HOMEO[Y CDR Z]->HOMEO[X CDR Z] (INDHYP)
=> HOMEO[X,CDR Z]
=> HOMEO[X,Z]
Case1.3 LISTP[Y] ∧ HOMEO[CAR Y,CAR Z] ∧ HOMEO[CDR Y,CDR Z]
Case1.3.1 HOMEO[X,CAR Y]
=> HOMEO[X CAR Y]∧ HOMEO[CAR Y CAR Z]->HOMEO[X CAR Z] (INDHYP)
=> HOMEO[X,CAR Z]
=> HOMEO[X,Z]
Case1.3.2 HOMEO[X,CDR Y]
=> HOMEO[X CDR Y]∧ HOMEO[CDR Y CDR Z]->HOMEO[X CDR Z] (INDHYP)
=> HOMEO[X,CDR Z]
=> HOMEO[X,Z]
Case1.3.3 LISTP[X] ∧ HOMEO[CAR X,CAR Y] ∧ HOMEO[CDR X,CDR Y]
=> HOMEO[CAR X CAR Y]∧ HOMEO[CAR Y CAR Z]->HOMEO[CAR X CAR Z] (INDHYP)
=> HOMEO[CDR X CDR Y]∧ HOMEO[CDR Y CDR Z]->HOMEO[CDR X CDR Z] (INDHYP)
=> LISTP[X] ∧ HOMEO[CAR X,CAR Z] ∧ HOMEO[CAR X,CAR Z]
=> HOMEO[X,Z]
DEFN(TRANS.HOMEO (X Y Z) (IF (HOMEO X Y) (IF (HOMEO Y Z) (HOMEO X Z) T) T))
DEFN(HO (X Y Z)
(IF (LISTP Z)
(OR (HO X Y (CAR Z))
(HO X Y (CDR Z))
(AND (LISTP Y)
(OR (HO X (CAR Y) (CAR Z))
(HO X (CDR Y) (CDR Z))
(AND (LISTP X)
(HO (CAR X) (CAR Y) (CAR Z))
(HO (CDR X) (CDR Y) (CDR Z)) ) )) )
T ))
The lemmas CAR.LESSP and CDR.LESSP establish that (COUNT Z)
decreases according to the well-founded function LESSP in each
recursive call. Hence, HO is accepted under the principle of
definition. Note that (TRUEP (HO X Y Z)) is a theorem.
PROVE( (IMPLIES (AND (HOMEO X Y) (HOMEO Y X)) (EQUAL X Y)) )
PROVE( (EQUAL (TRANS.HOMEO X Y Z) (HO X Y Z)) )
==>
(IMPLIES (AND (HOMEO X Y) (HOMEO Y Z))
(HOMEO X Z)),
DEFN(HOHO (X Y Z)
(IF (LISTP Z)
(OR (HOHO X Y (CAR Z))
(HOHO X Y (CDR Z))
(AND (LISTP Y)
(OR (HOHO X (CAR Y) (CAR Z))
(HOHO X (CDR Y) (CDR Z))
(AND (LISTP X)
(HOHO (CAR X) (CAR Y) (CAR Z))
(HOHO (CDR X) (CDR Y) (CDR Z)) ) )) )
(IMPLIES (AND (HOMEO X Y) (HOMEO Y Z)) (HOMEO X Z)) ))
The lemmas CAR.LESSP and CDR.LESSP inform us that (COUNT Z) goes
down according to the well-founded function LESSP in each recursive
call. Hence, HOHO is accepted under the principle of definition.
Observe that (OR (FALSEP (HOHO X Y Z)) (TRUEP (HOHO X Y Z))) is a
theorem.
[10201 cns / 7.9 s + 2.8 gc + .2 io (= 15 @ 1)]
HOHO
20:
PROVE((HOHO X Y Z))
Name the conjecture *1.
Perhaps we can prove it by induction. There is only one suggested
induction. We will induct according to the following scheme:
(AND (IMPLIES (NOT (LISTP Z)) (p X Y Z))
(IMPLIES (AND (LISTP Z)
(p (CDR X) (CDR Y) (CDR Z))
(p (CAR X) (CAR Y) (CAR Z))
(p X (CDR Y) (CDR Z))
(p X (CAR Y) (CAR Z))
(p X Y (CDR Z))
(p X Y (CAR Z)))
(p X Y Z))).
The inequalities CAR.LESSP and CDR.LESSP establish that the measure
(COUNT Z) decreases according to the well-founded function LESSP in the
induction step of the scheme. Note, however, the inductive instances
chosen for X and Y. The above induction scheme generates two new
conjectures:
Case 2. (IMPLIES (NOT (LISTP Z))
(HOHO X Y Z)),
which simplifies, expanding the functions HOMEO and HOHO, to the new
conjecture:
(IMPLIES (AND (NOT (LISTP Z))
(HOMEO X Y)
(EQUAL Y Z))
(EQUAL X Z)).
But this again simplifies, expanding the function HOMEO, to:
T.
Case 1. (IMPLIES (AND (LISTP Z)
(HOHO (CDR X) (CDR Y) (CDR Z))
(HOHO (CAR X) (CAR Y) (CAR Z))
(HOHO X (CDR Y) (CDR Z))
(HOHO X (CAR Y) (CAR Z))
(HOHO X Y (CDR Z))
(HOHO X Y (CAR Z)))
(HOHO X Y Z)),
which simplifies, expanding HOHO, to:
T.
That finishes the proof of *1. Q.E.D.
PROVED
21:
PROVE( (EQUAL (IMPLIES (AND (HOMEO X Y) (HOMEO Y Z)) (HOMEO X Z)) (HOHO X Y Z)) )
This conjecture simplifies, expanding the definitions of AND and
IMPLIES, to three new conjectures:
Case 3. (IMPLIES (NOT (HOMEO X Y))
(EQUAL T (HOHO X Y Z))),
which we again simplify, clearly, to the conjecture:
(IMPLIES (NOT (HOMEO X Y))
(HOHO X Y Z)),
which we will name *1.
collecting lists
12504, 12504 free cells
Case 2. (IMPLIES (NOT (HOMEO Y Z))
(EQUAL T (HOHO X Y Z))),
which we again simplify, clearly, to:
(IMPLIES (NOT (HOMEO Y Z))
(HOHO X Y Z)),
which we would normally push and work on later by induction. But if
we must use induction to prove the input conjecture, we prefer to
induct on the original formulation of the problem. Thus we will
disregard all that we have previously done, give the name *1 to the
original input, and work on it.
So now let's return to:
(EQUAL (IMPLIES (AND (HOMEO X Y) (HOMEO Y Z))
(HOMEO X Z))
(HOHO X Y Z)),
which we named *1 above. We will try to prove it by induction. The
recursive terms in the conjecture suggest four inductions. However,
they merge into one likely candidate induction. We will induct
according to the following scheme:
(AND (IMPLIES (NOT (LISTP Z)) (p X Y Z))
(IMPLIES (AND (LISTP Z)
(p (CDR X) (CDR Y) (CDR Z))
(p (CAR X) (CAR Y) (CAR Z))
(p X (CDR Y) (CDR Z))
(p X (CAR Y) (CAR Z))
(p X Y (CDR Z))
(p X Y (CAR Z)))
(p X Y Z))).
The inequalities CAR.LESSP and CDR.LESSP establish that the measure
(COUNT Z) decreases according to the well-founded function LESSP in the
induction step of the scheme. Note, however, the inductive instances
chosen for X and Y. The above induction scheme generates the following
two new goals:
Case 2. (IMPLIES (NOT (LISTP Z))
(EQUAL (IMPLIES (AND (HOMEO X Y) (HOMEO Y Z))
(HOMEO X Z))
(HOHO X Y Z))),
which simplifies, unfolding the functions HOMEO, AND, IMPLIES, and
HOHO, to the conjecture:
(IMPLIES (AND (NOT (LISTP Z))
(HOMEO X Y)
(EQUAL Y Z))
(EQUAL (EQUAL X Z) (EQUAL X Z))).
This simplifies again, unfolding the functions HOMEO and EQUAL, to:
T.
collecting lists
11423, 11423 free cells
collecting lists
10945, 10945 free cells
collecting lists
10148, 10148 free cells
collecting lists
9357, 10381 free cells
collecting lists
10054, 10054 free cells
collecting lists
9518, 10030 free cells
collecting lists
9317, 10341 free cells
collecting lists
9485, 10509 free cells
collecting lists
9843, 10355 free cells
collecting lists
9435, 10459 free cells
collecting lists
9567, 10079 free cells
collecting lists
9130, 10154 free cells
collecting lists
9966, 10478 free cells
collecting lists
9688, 10200 free cells
collecting lists
9801, 10313 free cells
collecting lists
9510, 10022 free cells
collecting lists
9743, 10255 free cells
collecting lists
9271, 10295 free cells
collecting lists
9866, 10378 free cells
collecting lists
9850, 10362 free cells
THM Running at 333677 Used 0:09:15.1 in 0:35:35, Load 1.37
collecting lists
9593, 10105 free cells
THM Running at 316050 Used 0:09:24.0 in 0:35:44, Load 1.32
collecting lists
9138, 10162 free cells
collecting lists
9155, 10179 free cells
collecting lists
9229, 10253 free cells
collecting lists
9914, 10426 free cells
collecting lists
THM Running at 30670 Used 0:10:09.2 in 0:36:32, Load 1.16
9779, 10291 free cells
collecting lists
9713, 10225 free cells
collecting lists
9595, 10107 free cells
collecting lists
9532, 10044 free cells
collecting lists
9641, 10153 free cells
collecting lists
9645, 10157 free cells
collecting lists
9812, 10324 free cells
collecting lists
9898, 10410 free cells
collecting lists
9445, 10469 free cells
collecting lists
10226, 10226 free cells
collecting lists
9840, 10352 free cells
collecting lists
9523, 10035 free cells
collecting lists
9200, 10224 free cells
THM Running at 4425 Used 0:12:12.6 in 0:38:46, Load 1.85
collecting lists
9575, 10087 free cells
collecting lists
9306, 10330 free cells, 40 pages left
collecting lists
9421, 10445 free cells, 38 pages left
collecting lists
9357, 10381 free cells, 36 pages left
collecting lists
9816, 10328 free cells, 35 pages left
collecting lists
10142, 10142 free cells, 35 pages left
collecting lists
9382, 10406 free cells, 33 pages left
collecting lists
9643, 10155 free cells, 32 pages left
collecting lists
9728, 10240 free cells, 31 pages left
collecting lists
9368, 10392 free cells, 29 pages left
collecting lists
9441, 10465 free cells, 27 pages left
collecting lists
9521, 10033 free cells, 26 pages left
collecting lists
7017, 10089 free cells, 20 pages left
Case 1. (IMPLIES
(AND (LISTP Z)
(EQUAL (IMPLIES (AND (HOMEO (CDR X) (CDR Y))
(HOMEO (CDR Y) (CDR Z)))
(HOMEO (CDR X) (CDR Z)))
(HOHO (CDR X) (CDR Y) (CDR Z)))
(EQUAL (IMPLIES (AND (HOMEO (CAR X) (CAR Y))
(HOMEO (CAR Y) (CAR Z)))
(HOMEO (CAR X) (CAR Z)))
(HOHO (CAR X) (CAR Y) (CAR Z)))
(EQUAL (IMPLIES (AND (HOMEO X (CDR Y))
(HOMEO (CDR Y) (CDR Z)))
(HOMEO X (CDR Z)))
(HOHO X (CDR Y) (CDR Z)))
(EQUAL (IMPLIES (AND (HOMEO X (CAR Y))
(HOMEO (CAR Y) (CAR Z)))
(HOMEO X (CAR Z)))
(HOHO X (CAR Y) (CAR Z)))
(EQUAL (IMPLIES (AND (HOMEO X Y) (HOMEO Y (CDR Z)))
(HOMEO X (CDR Z)))
(HOHO X Y (CDR Z)))
(EQUAL (IMPLIES (AND (HOMEO X Y) (HOMEO Y (CAR Z)))
(HOMEO X (CAR Z)))
(HOHO X Y (CAR Z))))
(EQUAL (IMPLIES (AND (HOMEO X Y) (HOMEO Y Z))
(HOMEO X Z))
(HOHO X Y Z))).
This simplifies, expanding AND, IMPLIES, HOMEO, HOHO, and EQUAL, to
953 new conjectures:
Case 1.953.
(IMPLIES (AND (LISTP Z)
(NOT (HOMEO (CDR X) (CDR Y)))
(EQUAL T
(HOHO (CDR X) (CDR Y) (CDR Z)))
(NOT (HOMEO (CAR X) (CAR Y)))
(EQUAL T
(HOHO (CAR X) (CAR Y) (CAR Z)))
(NOT (HOMEO X (CDR Y)))
(EQUAL T (HOHO X (CDR Y) (CDR Z)))
(NOT (HOMEO X (CAR Y)))
(EQUAL T (HOHO X (CAR Y) (CAR Z)))
(NOT (HOMEO Y (CDR Z)))
(EQUAL T (HOHO X Y (CDR Z)))
(NOT (LISTP Y))
(EQUAL X Y)
(HOMEO Y (CAR Z))
(EQUAL (HOMEO X (CAR Z))
(HOHO X Y (CAR Z)))
(NOT (HOMEO X (CAR Z))))
(HOMEO X (CDR Z))),
which again simplifies, clearly, to:
T.
Case 1.952.
(IMPLIES (AND (LISTP Z)
(NOT (HOMEO (CDR X) (CDR Y)))
(EQUAL T
(HOHO (CDR X) (CDR Y) (CDR Z)))
(NOT (HOMEO (CAR X) (CAR Y)))
(EQUAL T
(HOHO (CAR X) (CAR Y) (CAR Z)))
(NOT (HOMEO X (CDR Y)))
(EQUAL T (HOHO X (CDR Y) (CDR Z)))
(NOT (HOMEO X (CAR Y)))
(EQUAL T (HOHO X (CAR Y) (CAR Z)))
(NOT (LISTP Y))
(EQUAL X Y)
(HOMEO Y (CDR Z))
(EQUAL (HOMEO X (CDR Z))
(HOHO X Y (CDR Z)))
(NOT (HOMEO Y (CAR Z)))
(EQUAL T (HOHO X Y (CAR Z)))
(NOT (HOMEO X (CAR Z))))
(HOMEO X (CDR Z))),
which again simplifies, obviously, to:
T.
Case 1.951.
(IMPLIES (AND (LISTP Z)
(NOT (HOMEO (CDR X) (CDR Y)))
(EQUAL T
(HOHO (CDR X) (CDR Y) (CDR Z)))
(NOT (HOMEO (CAR X) (CAR Y)))
(EQUAL T
(HOHO (CAR X) (CAR Y) (CAR Z)))
(NOT (HOMEO X (CDR Y)))
(EQUAL T (HOHO X (CDR Y) (CDR Z)))
(NOT (HOMEO X (CAR Y)))
(EQUAL T (HOHO X (CAR Y) (CAR Z)))
(NOT (LISTP Y))
(EQUAL X Y)
(HOMEO Y (CDR Z))
(EQUAL (HOMEO X (CDR Z))
(HOHO X Y (CDR Z)))
(HOMEO Y (CAR Z))
(EQUAL (HOMEO X (CAR Z))
(HOHO X Y (CAR Z)))
(NOT (HOHO X Y (CAR Z)))
(HOMEO X (CAR Z)))
(EQUAL T (HOHO X Y (CDR Z)))),
which again simplifies, clearly, to:
T.
Case 1.950.
(IMPLIES (AND (LISTP Z)
(NOT (HOMEO (CDR X) (CDR Y)))
(EQUAL T
(HOHO (CDR X) (CDR Y) (CDR Z)))
(NOT (HOMEO (CAR X) (CAR Y)))
(EQUAL T
(HOHO (CAR X) (CAR Y) (CAR Z)))
(NOT (HOMEO X (CDR Y)))
(EQUAL T (HOHO X (CDR Y) (CDR Z)))
(NOT (HOMEO X (CAR Y)))
(EQUAL T (HOHO X (CAR Y) (CAR Z)))
(NOT (LISTP Y))
(EQUAL X Y)
(HOMEO Y (CDR Z))
(EQUAL (HOMEO X (CDR Z))
(HOHO X Y (CDR Z)))
(HOMEO Y (CAR Z))
(EQUAL (HOMEO X (CAR Z))
(HOHO X Y (CAR Z)))
(HOHO X Y (CAR Z))
(NOT (HOMEO X (CAR Z))))
(EQUAL (HOMEO X (CDR Z)) T)).
Of course, this simplifies again, clearly, to:
T.
Case 1.949.
(IMPLIES (AND (LISTP Z)
(NOT (HOMEO (CDR X) (CDR Y)))
(EQUAL T
(HOHO (CDR X) (CDR Y) (CDR Z)))
(NOT (HOMEO (CAR X) (CAR Y)))
(EQUAL T
(HOHO (CAR X) (CAR Y) (CAR Z)))
(NOT (HOMEO X (CDR Y)))
(EQUAL T (HOHO X (CDR Y) (CDR Z)))
(NOT (HOMEO (CAR Y) (CAR Z)))
(EQUAL T (HOHO X (CAR Y) (CAR Z)))
(NOT (HOMEO Y (CDR Z)))
(EQUAL T (HOHO X Y (CDR Z)))
(NOT (LISTP Y))
(EQUAL X Y)
(HOMEO Y (CAR Z))
(EQUAL (HOMEO X (CAR Z))
(HOHO X Y (CAR Z)))
(NOT (HOMEO X (CAR Z))))
(HOMEO X (CDR Z))).
This again simplifies, clearly, to:
T.
***CTRL-F ABORT***
************** F A I L E D **************
NIL
22: